Inference at * 
Iof proof for Lemma p-conditional-domain:


  A, B:Type, f, g:(A(B + Top)), x:A.
  (can-apply([f?g];x))  ((can-apply(f;x))  (can-apply(g;x))) 

latex

 by ((RepUR ``p-conditional can-apply`` ( 0)) 
CollapseTHEN (MaAuto)) 

latex

Co1: 

Co1: 1. A : Type
Co1: 2. B : Type
Co1: 3. f : A(B + Top)
Co1: 4. g : A(B + Top)
Co1: 5. x : A
Co1: 6. isl(if isl(f(x)) then f(x) else g(x) fi )
Co1: 7. (isl(f(x)))
Co1:   isl(g(x))
Co2: 

Co2: 1. A : Type
Co2: 2. B : Type
Co2: 3. f : A(B + Top)
Co2: 4. g : A(B + Top)
Co2: 5. x : A
Co2: 6. (isl(f(x)))  (isl(g(x)))
Co2:   isl(if isl(f(x)) then f(x) else g(x) fi )
Co.

Definitions	[f?g], can-apply(f;x), P  Q, P & Q, x:A  B(x), case b of inl(x) => s(x) | inr(y) => t(y), Dec(P), {T}, A, False, P  Q, P  Q, if b then t else f fi , P  Q, , b, isl(x), f(a), x:A. B(x), x:AB(x), left + right, Top, t  T, Type
Lemmas	decidable assert, ifthenelse wf, assert wf, isl wf, top wf